Logic Programming Systems The Conflict-Driven Answer Set Solver clasp       Martin Gebser, Benjamin Kaufmann, Torsten Schaub* Institut für Informatik Universität Potsdam     Germany Editor: Enrico Pontelli System Web Page: http://potassco.sourceforge.net PDF: Here The clasp system combines the high-level modeling capacities of Answer Set Programming (ASP; [1]) with state-of-the-art techniques from the area of Boolean constraint solving. clasp is designed and optimized for conflict-driven ASP solving [2,3]; it is freely available at http://potassco.sourceforge.net. Given the proximity of ASP to Satisfiability Checking (SAT), clasp can also deal with formulas in CNF via an additional DIMACS front-end.  As such, it can be viewed as a chaff-type Boolean constraint solver [4], encompassing conflict analysis via the First-UIP scheme, nogood recording and deletion, back-jumping, restarts, conflict-driven decision heuristics, unit propagation via watched literals, dedicated propagation of binary and ternary nogoods. clasp allows for computing all or at most a given number of answer sets by means of a dedicated enumeration algorithm [5]; also, it allows for computing the intersection or union, respectively, of all answer sets (in a linear way). For supporting the high-level modeling capacities of ASP, clasp offers special Boolean constraint techniques for dealing with aggregates, like cardinality and weight constraints, optimization statements, and incremental reasoning, needed for planning, model checking, and alike. A given logic program is (by default) subject to advanced preprocessing techniques [6], involving equivalence detection, before it is transformed into Boolean constraints following Clark's completion. The resulting nogoods are then subject to further preprocessing techniques adapted from the area of SAT. Special mention deserves the detection of unfounded sets [7],  aiming at small and "loop-encompassing" rather than greatest unfounded sets, as done traditionally. Meanwhile, clasp has been extended in several ways. claspD [8] extends clasp to disjunctive logic programming, Clingo is a monolithic combination of the ASP grounder GrinGo [9] and clasp, and iClingo [10] is an incremental ASP system implemented on top of Clingo. References [1] Baral, C.: Knowledge Representation, Reasoning and Declarative Problem Solving. Cambridge University Press (2003) [2] Gebser, M., Kaufmann, B., Neumann, A., Schaub, T.: Conflict-driven answer set solving. In Veloso, M., ed.: Proceedings of the Twentieth International Joint Conference on Artificial Intelligence (IJCAI'07), AAAI Press/The MIT Press (2007)  386--392. [3] Gebser, M., Kaufmann, B., Neumann, A., Schaub, T.: clasp: A conflict-driven answer set solver. [11], 260--265 [4] Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.:Chaff: Engineering an efficient SAT solver. In: Proceedings of the Thirty-eighth Conference on Design Automation (DAC'01), ACM Press (2001)  530--535 [5] Gebser, M., Kaufmann, B., Neumann, A., Schaub, T.: Conflict-driven answer set enumeration. \newblock  [11], 136--148 [6] Gebser, M., Kaufmann, B., Neumann, A., Schaub, T.: Advanced preprocessing for answer set solving. In Ghallab, M., Spyropoulos, C., Fakotakis, N., Avouris, N., eds.: Proceedings of the Eighteenth European Conference on Artificial Intelligence (ECAI'08), IOS Press (2008)  15--19 [7] Anger, C., Gebser, M., Schaub, T.: Approaching the core of unfounded sets.In Dix, J., Hunter, A., eds.: Proceedings of the Eleventh International Workshop on Nonmonotonic Reasoning (NMR'06). Number IFI-06-04 in Technical Report Series, Clausthal University of Technology, Institute for   Informatics (2006)  58--66 [8] Drescher, C., Gebser, M., Grote, T., Kaufmann, B., König, A., Ostrowski, M., Schaub, T.: Conflict-driven disjunctive answer set solving.In Brewka, G., Lang, J., eds.: Proceedings of the Eleventh  International Conference on Principles of Knowledge Representation and Reasoning (KR'08), AAAI Press (2008)  422--432 [9] Gebser, M., Schaub, T., Thiele, S.: GrinGo: A new grounder for answer set programming. [11],  266--271 [10] Gebser, M., Kaminski, R., Kaufmann, B., Ostrowski, M., Schaub, T., Thiele, S.: Engineering an incremental ASP solver.  In Garcia de la Banda, M., Pontelli, E., eds.: Proceedings of the Twenty-fourth International Conference on Logic Programming (ICLP'08). Volume 5366 of Lecture Notes in Computer Science., Springer-Verlag (2008) To appear. [11] Baral, C., Brewka, G., Schlipf, J., eds.:Proceedings of the Ninth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'07). Volume 4483 of Lecture Notes in Artificial Intelligence., Springer-Verlag (2007). * Affiliated with Simon Fraser University, Canada, and Griffith University, Australia.